『The Type Theory of Lean』
1. どんなもの？
2. 先行研究と比べてどこがすごい？
3. 技術や手法のキモはどこ？
4. どうやって有効だと検証した？
5. 議論はある？
6. 次に読むべき論文は？
table:単語
dependent type 依存型
subsingleton elimination 準単集合消去
propositional extensionality 命題的外延性
axiom of choice 選択公理
inaccessible cardinal 到達不能基数
Church-Rosser property Church-Rosser性
non-transitive 非推移的
undecidable 決定不可能
underapproximation 過小近似
normal form 正規形
typing 型付け
term 項
context 文脈
universe 宇宙
inductive type 帰納型
recursor 再帰子
constructor 構築子
predicate 述語
proof 証明
equality 等式？
bijection 全単射
sort function ソート関数
level expression レベル表現
universe variable 宇宙変数
well-typed 型付けされた
type preservation 型保存
translation rule 翻訳規則
eliminator 除去子
parametricity パラメトリシティ
small elimination 小除去
large elimination 大除去
ZFC translation ZFC翻訳
η rule イータ規則
β reduction ベータ簡約
κ reduction カッパ簡約
ι reduction イオタ簡約
ζ reduction ゼータ簡約
algorithmic equivalence アルゴリズム的同値
well-founded recursion 整礎再帰 accumulator 累積変数
dependent type theory 依存型理論
inductive type 帰納型
universe hierarchy 宇宙の階層
universe 宇宙（型の階層）
impredicative universe 非可述的宇宙
prop (proposition universe) 命題の宇宙（Prop）
subsingleton elimination サブシングルトン消去
propositional extensionality 命題外延性
axiom of choice (AC) 選択公理（AC）
quotient type 商型
type theory 型理論
lean theorem prover Lean定理証明支援系
definitional equality 定義的等価性
algorithmic equality アルゴリズム的等価性
type checking 型検査
subject reduction 主語簡約性
church-rosser property チャーチ–ロッサー性
normal form 正規形
reduction relation 簡約関係
unique typing 一意型付け
set-theoretic model 集合論的モデル
zfc (zermelo–fraenkel set theory with choice) ZFC集合論
inaccessible cardinal 到達不能基数
large cardinal assumption 大型基数仮定
w-type W型
cumulative hierarchy 累積階層
grothendieck universe グロタンディーク宇宙
impredicativity 非述語性
predicative 述語的
partial equivalence relation (PER) 部分同値関係（PER）
curry-howard isomorphism カリー＝ハワード同型
simply typed lambda calculus 単純型付きラムダ計算
dependent type 依存型
calculus of constructions (CoC) 構成の計算（CoC）
calculus of inductive constructions (CIC) 帰納構成の計算（CIC）
recursor 再帰子
eliminator 消去子
large elimination 大消去
small elimination 小消去
computation rule 計算規則
beta reduction (β reduction) ベータ簡約（β簡約）
eta rule (η rule) イータ規則（η規則）
iota reduction (ι reduction) イオタ簡約（ι簡約）
zeta reduction (ζ reduction) ゼータ簡約（ζ簡約）
delta reduction (δ reduction) デルタ簡約（δ簡約）
k-like reduction K様簡約
axiom k (UIP) 公理K（同一性証明の一意性, UIP）
univalence 単価性
homotopy type theory (HoTT) ホモトピー型理論（HoTT）
well-founded recursion 整礎再帰
accessibility (acc) 可到達性（acc）
well-founded relation 整礎関係
universe polymorphism 宇宙多相性
cumulativity 累積性
fixpoint (fix) 不動点（fix）
pattern matching パターンマッチング
setoid セトイド
law of excluded middle (LEM) 排中律（LEM）
global choice function 大域的選択関数
nonempty 非空
regularity 正則性
weakening 弱化
substitution 代入
確認用
Q.